Skip to content

[Merged by Bors] - feat: vector measures with density wrt vector measures#41080

Closed
sgouezel wants to merge 2 commits into
leanprover-community:masterfrom
sgouezel:SG_densVec
Closed

[Merged by Bors] - feat: vector measures with density wrt vector measures#41080
sgouezel wants to merge 2 commits into
leanprover-community:masterfrom
sgouezel:SG_densVec

Conversation

@sgouezel

@sgouezel sgouezel commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

Open in Gitpod

@github-actions

github-actions Bot commented Jun 26, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 1cbb9fd002

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.MeasureTheory.VectorMeasure.WithDensityVec (new file) 2348

Declarations diff (regex)

+ _root_.MeasureTheory.Measure.variation_withDensityᵥ
+ restrict_withDensity
+ variation_WithDensity_le
+ variation_withDensity
+ variation_withDensity'
+ withDensity
+ withDensity_apply
+ withDensity_apply_univ
+ withDensity_congr
+ withDensity_zero
+ withDensity_zero_vectorMeasure

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 1cbb9fd).

  • +12 new declarations
  • −0 removed declarations
+MeasureTheory.Measure.variation_withDensityᵥ
+MeasureTheory.VectorMeasure.restrict_withDensity
+MeasureTheory.VectorMeasure.variation_WithDensity_le
+MeasureTheory.VectorMeasure.variation_withDensity
+MeasureTheory.VectorMeasure.variation_withDensity'
+MeasureTheory.VectorMeasure.withDensity
+MeasureTheory.VectorMeasure.withDensity_apply
+MeasureTheory.VectorMeasure.withDensity_apply_univ
+MeasureTheory.VectorMeasure.withDensity_congr
+MeasureTheory.VectorMeasure.withDensity_fun_zero
+MeasureTheory.VectorMeasure.withDensity_zero
+MeasureTheory.VectorMeasure.withDensity_zero_vectorMeasure

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type (weak)
4974 1 exposed public sections

Current commit 1cbb9fd002
Reference commit 571b8a8e54

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-measure-probability Measure theory / Probability theory label Jun 26, 2026
@sgouezel sgouezel mentioned this pull request Jun 26, 2026
Draft
29 tasks
RemyDegenne
RemyDegenne approved these changes Jun 29, 2026
View reviewed changes

@RemyDegenne RemyDegenne left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors r+

@mathlib-bors mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jun 29, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Jun 29, 2026
@sgouezel
feat: vector measures with density wrt vector measures (#41080)
7a9fb52 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@mathlib-bors mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jun 29, 2026
@mathlib-bors

mathlib-bors Bot commented Jun 29, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat: vector measures with density wrt vector measures [Merged by Bors] - feat: vector measures with density wrt vector measures Jun 29, 2026
@mathlib-bors mathlib-bors Bot closed this Jun 29, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@RemyDegenne RemyDegenne RemyDegenne approved these changes

Assignees

No one assigned

Labels

bors-staging This PR is currently being built by bors on the staging branch. ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@sgouezel @RemyDegenne